\documentclass[]{article}


\usepackage[latin1]{inputenc}
\usepackage[english]{babel}

\usepackage{amstext, amssymb, amsfonts}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{myproof}

\newcommand{\ho}[2]{#1\langle #2 \rangle}
\newcommand{\inp}[2]{#1(#2)}
\newcommand{\nest}{nest}
\newcommand{\nil}{{\bf 0}}
\newcommand{\depth}{dep_x}
\newcommand{\bv}{bv}
\newcommand{\fv}{fv}
\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}


\newtheorem{theorem}{Theorem}
\newtheorem{definition}[theorem]{Definition}


\begin{document}


\section{Calculus}

$$
\begin{array}{rcl}
P & :: = &  \ho{a}{ P}  \\
 & \mid &  \inp{a}{x} . P \\
 & \mid &  P \parallel P \\
 & \mid &  x  \\
 & \mid & \nil 
 \end{array} 
$$


\section{Measures}

\begin{definition}[Nesting of $P$]
Maximal nesting of a process (counting both inputs and outputs)

$$
\begin{array}{rcl}
\nest(  \ho{a}{ P} )& ::=  &1 + \nest(P) \\
\nest(  \inp{a}{ P}) & ::=  &1 + \nest(P) \\
\nest( P \parallel Q ) & ::=  & max( \nest(P), \nest(Q)) \\
\nest(x) & ::=  & 0 \\
\nest( \nil) & ::=  &0
 \end{array} 
$$

\end{definition}



\begin{definition}[Depth of $x$ in $P$]
Maximal nesting of $x$ in an output

$$
\begin{array}{rcl}
\depth(  \ho{a}{ P} )& ::=  &2 *  \depth(P) \\
\depth(  \inp{a}{ P}) & ::=  &2 * \depth(P) \\
\depth( P \parallel Q ) & ::=  & max( \depth(P), \depth(Q)) \\
\depth(y) & ::=  & 1   \quad \text{if } x = y \\
\depth(y) & ::=  & 0  \quad   \text{if } x \neq y \\
\depth( \nil) & ::=  &0
 \end{array} 
$$

\end{definition}


\section{Semantics}

$$\mathrm{\textsc{Inp}}~~~{\inp{ a}{ x}. P} \xrightarrow{\inp{ a}{ x}  }  {P } \qquad \qquad \mathrm{\textsc{Out}}~~~{\ho{a}{P}} \xrightarrow{\ho{ a}{ P}  }  {\nil}$$
$$
\rightinfer	[\textsc{Act1}]
			{P_1 \parallel P_2 \xrightarrow{\alpha} P'_1 \parallel P_2}
			{P_1 \xrightarrow{\alpha} P_1'  \qquad \bv (\alpha) \cap \fv( P_2) = \emptyset}
$$
$$
\rightinfer	[\textsc{Tau1}]
			{P_1 \parallel P_2 \xrightarrow{\tau}  P'_1 \parallel P'_2 \sub{P}{x}}
			{P_1 \xrightarrow{\ho{a}{P}} P_1' \qquad P_2 \xrightarrow{\inp{a} {x}} P'_2
			\qquad \nest(P) + log_2(\depth(P_2'))\leq k }
$$

where $k$ is a given constant.


\end{document}